Inversion

Syntax directed means for each type, there’s only rule that can introduce it. E.g. the only way to introduce the plus syntax is using the PLUS rule.

We call these inversion lemmata:

Can be proven by (but doesn’t need to proven in exam):

• Proof by Induction
• Inspection

Weakening

Adding unrelated variables to the environment should not affect typing. Holds for most programming languages.

If you end up with two different environments, you can use weakening.

Substitution

Substitution is a [[meta-theoretic operation]].

Barendregt Convention

We assume that everything has been alpha renamed already so this doesn’t happen. Basically we just assume this won’t be a problem.

Substitution Lemma

To ensure substitution plays nicely with our language:

Related Reading

• 2025-09-30 Statics

Cards

Q: What is weakening? A: Adding unrelated variables to the environment should not affect typing. Can be used to say two statements are equivalent if they only have different environments.

Q: What is the inversion lemma? A: If you have an expression of form according to the conclusion of some rule, the types from the premise hold.